composite_R_eq
plain-language theorem explainer
The equality shows that the recognition map of a composite recognizer is the ordered pair of the maps of its two components. Workers on the refinement theorem and multi-measurement systems in Recognition Geometry cite this when manipulating composite maps. The proof is immediate reflexivity on the definition of the tensor product of recognizers.
Claim. For recognizers $r_1 : C → E_1$ and $r_2 : C → E_2$, the composite recognizer satisfies $(r_1 ⊗ r_2).R(c) = (r_1.R(c), r_2.R(c))$ for any configuration $c ∈ C$.
background
In the Recognition Geometry module on composition (RG6), a recognizer is a map from a configuration space C to an event space. The composite recognizer $r_1 ⊗ r_2$ is constructed so that its recognition map returns the ordered pair of the individual recognition values. This module develops how combining recognizers refines the indistinguishability relation, producing larger quotients and richer geometry from multiple measurements.
proof idea
The proof is a one-line term proof by reflexivity that matches the definition of the composite recognizer's map directly to the product of the component maps.
why it matters
This equality is the base fact used to prove composite_indistinguishable_iff (indistinguishability under the composite is the conjunction of the two component relations) and composite_distinguishes (the composite separates any pair separated by either factor). It is invoked in the module's refinement theorem and in downstream dimension results such as independent_strict_refines and pairSeparates_iff. Within the Recognition Science framework it supports the emergence of geometry from multiple measurements as outlined in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.