quotientMapRight
plain-language theorem explainer
quotientMapRight constructs the natural projection from the recognition quotient of the composite recognizer r₁ ⊗ r₂ onto the quotient of r₂. Researchers establishing the refinement theorem in recognition geometry cite this map to show that composite measurements yield surjective projections onto component quotients. The definition is realized by lifting the canonical projection recognitionQuotientMk r₂ through the equivalence relation, using the fact that composite indistinguishability implies r₂-indistinguishability.
Claim. Let $r_1 : Recognizer(C, E_1)$ and $r_2 : Recognizer(C, E_2)$. There is a map $C_{r_1 ⊗ r_2} → C_{r_2}$ sending each equivalence class under the composite indistinguishability relation to its class under the $r_2$-indistinguishability relation.
background
The module develops the geometry of composite recognizers. A Recognizer assigns to each configuration in C an event in E. Two configurations are indistinguishable under r if they map to the same event. The RecognitionQuotient is the set of equivalence classes under this relation, with recognitionQuotientMk the canonical projection. Composite recognizers are formed as pairs, and upstream results establish that indistinguishability under the composite implies indistinguishability under each component separately. In particular, composite_refines_right shows that if c1 ~{r1 ⊗ r2} c2 then c1 ~{r2} c2. quotientMk_eq_iff equates equality of quotient elements with indistinguishability. This setting allows maps between quotients to be defined by lifting projections when the equivalence relations are compatible.
proof idea
The definition applies Quotient.lift to recognitionQuotientMk r₂. The proof obligation that the lift is well-defined is discharged by reducing class equality to indistinguishability via quotientMk_eq_iff and then applying composite_refines_right to obtain the required indistinguishability under r₂.
why it matters
This definition supplies one of the two projection maps in the refinement theorem, which states that the composite quotient surjects onto each component quotient. It is invoked in the paper-level theorem refinement and the corollary pillar2_composite_refines. Within Recognition Science it contributes to showing how multiple recognizers produce a finer partition of configuration space, aligning with the emergence of geometry from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.