composite_comm_events
plain-language theorem explainer
Composition of two recognizers is commutative up to swapping output events: the joint recognition map of r1 tensor r2 at c equals the swapped pair from r2 tensor r1. Researchers modeling joint measurements or refinement in recognition geometry cite this for symmetry of composite systems. The proof is a one-line simplification that invokes the product definition of the composite map.
Claim. For recognizers $r_1: C → E_1$ and $r_2: C → E_2$, the composite recognition map satisfies $(r_1 ⊗ r_2)(c) = swap((r_2 ⊗ r_1)(c))$.
background
Recognition Geometry develops how multiple recognizers act jointly on a shared configuration space C. The composite recognizer is defined by the product map that sends each configuration c to the pair of individual outputs, which refines indistinguishability to the intersection of the component relations and enlarges the quotient space. The module RG6 establishes the Refinement Theorem showing that the composite quotient is finer than either factor alone.
proof idea
The proof is a one-line wrapper that applies the product definition of the composite map from the upstream result composite_R_eq and observes the swap symmetry.
why it matters
This commutativity lemma supports symmetry properties inside the Refinement Theorem of the module. It aligns with the Recognition Composition Law by ensuring that the order of combining measurements does not alter the joint event structure up to isomorphism. The result closes a basic symmetry gap in the construction of richer geometry from simpler recognizers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.