quotient_uniqueness
plain-language theorem explainer
The recognition quotient induced by any recognizer r is surjective onto its image while the induced event map remains injective, establishing uniqueness up to isomorphism. Categorical geometers and recognition theorists cite this corollary for the coequalizer property of the indistinguishability relation. The proof is a one-line term extraction of the two required components from the universal_property lemma.
Claim. Let $C$ be a configuration space and $E$ an event space. For any recognizer $r$, the canonical projection $C$ to the recognition quotient $C_R$ is surjective and the induced map $C_R$ to $E$ is injective.
background
Recognition Geometry defines the recognition quotient $C_R$ as the set of equivalence classes of configurations under the indistinguishability relation generated by a recognizer. The module states three pillars: the quotient determines observables, additional recognizers increase distinguishing power, and finite resolution forces coarse-graining. The local setting is the Emergence Principle that observable space arises exactly from recognition relationships, with the fundamental theorem asserting $[c_1] = [c_2]$ in $C_R$ if and only if $r(c_1) = r(c_2)$.
proof idea
One-line term proof that applies the universal_property lemma and projects out its first component for surjectivity together with the first part of its second component for injectivity of the event map.
why it matters
This corollary confirms the recognition quotient is terminal among quotients admitting an injective factorization, directly supporting the Emergence Principle that space is the structure of what can be recognized. It fills the uniqueness half of the Fundamental Theorem in the module and justifies why spacetime dimension and gauge symmetries arise from independent recognizers and recognition-preserving maps. The result closes the categorical foundation before the finite-resolution and composite-refinement pillars are developed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.