quotientMk_respects_event
plain-language theorem explainer
quotientMk_respects_event asserts that configurations identified under the recognition quotient map share identical recognizer outputs. It is invoked when constructing the induced event map on the quotient space in recognition geometry. The proof is a one-line term that applies the defining equivalence quotientMk_eq_iff via modus ponens.
Claim. Let $r : C → E$ be a recognizer on a configuration space $C$. If the quotient projections satisfy $π_r(c_1) = π_r(c_2)$, then $r(c_1) = r(c_2)$.
background
The module defines the recognition quotient $C_R = C / ∼$ where $c_1 ∼ c_2$ precisely when the recognizer $R$ returns the same event value. A configuration space supplies an empty element, a commutative join, a consistency predicate, and an independence relation, as stated in the ConfigSpace class. The theorem is the direct statement that the canonical projection respects this equivalence relation induced by $R$.
proof idea
The proof is a one-line wrapper that applies (quotientMk_eq_iff r).mp h, unfolding the hypothesis that the two configurations lie in the same equivalence class.
why it matters
The result guarantees that the event map factors through the quotient as $R = R̄ ∘ π$, which is required for the subsequent definitions of quotientEventMap and liftToQuotient. It closes the basic compatibility step in the RecognitionQuotient construction and aligns with the framework's use of indistinguishability to collapse configurations while preserving observable events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.