IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Quotient
Defines the setoid of recognition endpoints under the SameT relation at a fixed trace, and the associated quotient type of endpoint classes. Anyone working with K2.11 or the primitive recognition calculus cites this when collapsing observationally equivalent endpoints. The module is definitional: it packages the setoid, the quotient, and the standard lift lemmas.
claimAt a fixed trace $T$, the relation $\mathrm{SameT}$ induces a setoid on recognition endpoints. Write $[e]$ for the equivalence class of an endpoint $e$ (the endpoint class). Two endpoints determine the same class precisely when they are $\mathrm{SameT}$-related, and maps constant on $\mathrm{SameT}$-classes lift uniquely through the quotient.
background
Primitive recognition calculus treats endpoints of recognition processes as the raw observational data. The upstream module SameDiff supplies the relation SameT: two endpoints are identified when they agree on the fixed-trace recognition data that the calculus treats as indistinguishable.
A setoid is an equivalence relation packaged for Lean's quotient construction. Here the carrier is the type of endpoints at a fixed trace, and the relation is SameT. The quotient type EndpointClass is the space of observational equivalence classes; endpointClassOf sends an endpoint to its class.
The local setting is K2.11 of the foundation layer: before one can state a recognition kernel or a cost functional on observations, one must pass to the quotient so that the functional depends only on SameT-classes, not on representative choice.
proof idea
This is a definition module, not a theorem module. It introduces sameSetoid from the SameT relation, defines EndpointClass as the corresponding quotient, and records the standard API: endpointClassOf, equality of classes from SameT (endpointClass_eq_of_same), and the universal property of the quotient via endpointClassLift and endpointClassLift_mk. No deep proof content; the work is packaging Mathlib's setoid/quotient interface around SameT.
why it matters in Recognition Science
Kernel imports this module, so every subsequent statement about the recognition kernel is stated on endpoint classes rather than raw endpoints. That is the point of K2.11: cost, defect, and forcing data must be invariant under SameT, and the quotient is the clean carrier for that invariance.
In the broader Recognition Science stack this sits early in the foundation layer, before J-cost uniqueness (T5), the phi fixed point (T6), and the eight-tick and dimension forcings (T7–T8). Without collapsing SameT-equivalent endpoints, later uniqueness and forcing arguments would be forced to carry spurious representative dependence.
scope and limits
- Does not prove that SameT is an equivalence relation; that is assumed from SameDiff.
- Does not define the recognition kernel or any cost functional on classes.
- Does not force phi, J-uniqueness, dimension, or the eight-tick structure.
- Does not identify endpoint classes with physical states or measurement outcomes.
- Does not address traces other than the fixed trace at which SameT is taken.