composite_refines_right
plain-language theorem explainer
If two configurations are indistinguishable under the product recognizer r1 ⊗ r2, then they remain indistinguishable under r2 alone. Researchers constructing quotient maps or proving refinement properties in Recognition Geometry would cite this when showing that composite measurements produce finer equivalence relations. The proof is a one-line term that extracts the right conjunct from the biconditional supplied by composite_indistinguishable_iff.
Claim. If $c_1$ and $c_2$ satisfy $c_1 ~[r_1 ⊗ r_2] c_2$, then $c_1 ~[r_2] c_2$.
background
Recognition Geometry treats physical measurement as the action of a recognizer that maps configurations to events. Two configurations are indistinguishable under a recognizer precisely when they produce identical events, yielding the fundamental equivalence relation of the theory. The present module develops composite recognizers formed by pairing two recognizers on the same configuration space, with the explicit goal of showing that the composite induces a strictly finer indistinguishability relation than either factor.
proof idea
One-line wrapper that applies composite_indistinguishable_iff to the hypothesis and projects onto the second conjunct.
why it matters
The result is invoked directly in the definition of quotientMapRight, which lifts maps from the composite quotient to the r2 quotient. It therefore supplies one half of the Refinement Theorem stated in the module documentation, confirming that richer geometry emerges from the simultaneous action of multiple recognizers. The construction sits inside the broader Recognition Science program in which composite measurements enlarge the set of distinguishable classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.