quotientEventMap_injective
plain-language theorem explainer
The induced map from the recognition quotient to the event space is injective. Researchers citing the universal property of the recognition quotient or the injectivity of observable maps in Recognition Geometry would reference this result. The argument lifts two quotient elements to representatives, reduces the hypothesis via simplification to equality of their images under R, and applies the quotient soundness axiom to conclude the classes coincide.
Claim. Let $C_R$ denote the recognition quotient of a configuration space $C$ under the indistinguishability relation induced by a recognizer $R: C → E$. The induced map $C_R → E$ sending each equivalence class to the common value of $R$ on its members is injective.
background
The module defines the recognition quotient $C_R = C / ∼$ where $c_1 ∼ c_2$ precisely when $R(c_1) = R(c_2)$, collapsing configurations that the recognizer cannot distinguish. This construction appears after the definition of RecognitionQuotient and the canonical projection. Upstream results include the soundness theorems for quotients of integers and rationals from logic, which establish that the quotient respects the defining equivalence, and structures such as LedgerFactorization.of that calibrate the underlying J-cost.
proof idea
The term proof introduces quotient elements q₁ and q₂ together with the assumption that their images under quotientEventMap coincide. It obtains representatives c₁ and c₂ via Quotient.exists_rep, simplifies the hypothesis to R c₁ = R c₂, and concludes by applying Quotient.sound.
why it matters
The result is invoked directly by pillar1_quotient_determines_observables, the universal_property theorem, and injectivity_of_observable_map in DraftV1. It supplies the injectivity half of the recognition_quotient_summary and confirms that the quotient is the finest space through which R factors injectively. In the Recognition Science setting this supports the claim that observables determine equivalence classes uniquely, consistent with the Recognition Composition Law and the forcing chain from T5 onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.