pillar1_quotient_determines_observables
plain-language theorem explainer
The result establishes that the event map induced by any recognizer on the recognition quotient is injective, so distinct equivalence classes produce distinct observable events. Researchers formalizing the foundations of Recognition Geometry cite it as Pillar 1, the statement that observables uniquely recover the quotient classes. The proof is a direct one-line application of the underlying injectivity lemma for the quotient event map.
Claim. Let $C$ be a configuration space and $E$ an event space. For any recognizer $r$ from $C$ to $E$, the induced map from the recognition quotient $C_R$ to $E$ is injective: if two classes map to the same event then the classes coincide.
background
A configuration space equips a type with an empty element, a commutative join operation, a consistency predicate, and an independence relation obeying monoid laws, as defined in the ConfigSpace class. An event space serves as the codomain for recognizers that assign observable events to configurations. The module states the three pillars of Recognition Geometry; this declaration is the first, asserting that the quotient $C_R$ encodes exactly the observable distinctions via the equivalence $[c_1] = [c_2]$ in $C_R$ if and only if $r(c_1) = r(c_2)$.
proof idea
The proof is a one-line wrapper that applies the injectivity lemma quotientEventMap_injective directly to the recognizer r.
why it matters
This is Pillar 1, feeding the foundations_status corollary that identifies the recognition quotient as the universal coequalizer of the indistinguishability relation. It fills the module's claim that the observable geometry is completely determined by the family of recognizers and aligns with the Recognition Science emphasis on quotients capturing observables without reference to the phi-ladder or spatial dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.