quotient_equiv_image
The declaration defines a canonical bijection between the recognition quotient and the image of the recognizer map R. Modelers of observable spaces in Recognition Science cite it to equate the collapsed configuration space with the set of distinguishable events. The construction exhibits an explicit equivalence via the lifted event map and verifies bijectivity from the map's injectivity and specification properties.
claimLet $R: C → E$ be a recognizer. The recognition quotient $C/∼_R$, where $c_1 ∼_R c_2$ if and only if $R(c_1)=R(c_2)$, is canonically equivalent to the image of $R$.
background
The Recognition Geometry module constructs the recognition quotient as the quotient of configuration space $C$ by the indistinguishability relation induced by a recognizer $R: C → E$. Two configurations are identified precisely when they produce the same event under $R$. The quotientEventMap lifts $R$ to a well-defined map on the quotient, satisfying $R = R̄ ∘ π$ where π is the canonical projection.
proof idea
The definition builds the equivalence with Equiv.ofBijective. The forward direction sends a quotient class q to the subtype element (quotientEventMap r q, witness) obtained by induction on representatives. Injectivity applies quotientEventMap_injective. Surjectivity recovers a representative via quotientEventMap_spec and recognitionQuotientMk.
why it matters in Recognition Science
This equivalence is applied in physical_space_is_quotient (RSBridge) to obtain that observable space is isomorphic to the image of a measurement map, realizing the statement “observable space ≅ Im(R)”. It also supports the summary in quotient_status. The result closes the geometric identification of the quotient with distinguishable events in the Recognition Geometry layer.
scope and limits
- Does not equip the quotient with topology or metric structure.
- Does not relate the equivalence to J-cost or the phi-ladder.
- Does not prove uniqueness of the bijection beyond the explicit construction.
- Does not extend the result to categorical or higher-dimensional settings.
Lean usage
simpa [toRecognizer] using (quotient_equiv_image (r := toRecognizer m))formal statement (Lean)
76noncomputable def quotient_equiv_image :
77 RecognitionQuotient r ≃ Set.range r.R :=
proof body
Definition body.
78 Equiv.ofBijective
79 (fun q => ⟨quotientEventMap r q,
80 Quotient.inductionOn q (fun c => ⟨c, rfl⟩)⟩)
81 ⟨fun q₁ q₂ h => by
82 simp only [Subtype.mk.injEq] at h
83 exact quotientEventMap_injective r h,
84 fun ⟨e, c, hc⟩ => ⟨recognitionQuotientMk r c, by simp [quotientEventMap_spec, hc]⟩⟩
85
86/-! ## Lifting Functions to Quotient -/
87
88/-- A function f : C → X descends to the quotient if it respects indistinguishability -/