quotient_equiv_image
plain-language theorem explainer
The definition shows the recognition quotient is canonically isomorphic to the image of the recognizer map R. A researcher modeling observable events from indistinguishable configurations would cite it to equate the quotient with measurable outcomes. The proof builds the bijection by sending quotient classes to their R-images and inverting via canonical lifts.
Claim. Let $C_R$ be the quotient of configuration space $C$ by the indistinguishability relation induced by a recognizer $R: C → E$. Then $C_R$ is isomorphic to the image of $R$, written $C_R ≃ im(R)$.
background
Recognition Geometry constructs the recognition quotient $C_R = C / ∼$ where $c_1 ∼ c_2$ precisely when $R(c_1) = R(c_2)$. The canonical projection $π: C → C_R$ collapses indistinguishable configurations. The induced event map $R̄: C_R → E$ satisfies $R = R̄ ∘ π$ and is injective on the quotient. Upstream results supply the integer and rational constructors from logic, the active-edge count $A = 1$, and the actualization operator, all used to ground the recognizer in the broader RS foundation.
proof idea
The definition applies Equiv.ofBijective. The forward direction maps a quotient element $q$ to the subtype element $(quotientEventMap r q, witness)$ obtained by induction on representatives. Injectivity uses the already-proved injectivity of quotientEventMap. Surjectivity lifts any element of the image back to a quotient class via recognitionQuotientMk and the specification lemma for the event map.
why it matters
This isomorphism is invoked directly by physical_space_is_quotient to identify observable physical space with the image of a measurement map, and it appears in the summary theorem quotient_status that records the quotient as capturing exactly the observable structure. It realizes the module-level claim that the quotient collapses configurations indistinguishable by R, aligning with the Recognition Science emphasis on quotients by indistinguishability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.