composite_comm_indistinguishable
plain-language theorem explainer
Indistinguishability under a composite recognizer is invariant under swapping the order of the two component recognizers. Researchers working on recognition geometry or composite measurement models would cite this symmetry result when establishing that the order of composition does not affect the equivalence classes. The proof is a one-line tactic that rewrites both sides using the characterization of composite indistinguishability and invokes commutativity of conjunction.
Claim. For recognizers $r_1$ and $r_2$ with event spaces $E_1$ and $E_2$, and configurations $c_1, c_2$ in the common domain $C$, $c_1$ is indistinguishable from $c_2$ under the product recognizer $r_1$ tensor $r_2$ if and only if they are indistinguishable under $r_2$ tensor $r_1$.
background
Recognition geometry studies how multiple recognizers act on the same configuration space $C$. A recognizer maps each configuration to an event; two configurations are indistinguishable under it precisely when they map to the same event. Composite recognizers are formed by the product map, so the composite sends $c$ to the pair of events produced by each component. The module develops the theory of such products and proves that the composite distinguishes at least as much as either factor alone, yielding a finer equivalence relation and a larger quotient space.
proof idea
The proof rewrites both sides of the biconditional via the supporting lemma that equates composite indistinguishability to the conjunction of the two component indistinguishabilities. It then applies the commutativity of logical conjunction to obtain the desired equivalence.
why it matters
The result establishes commutativity of the indistinguishability relation under composition, ensuring equivalence classes are independent of recognizer order. It supports the refinement theorem developed in the same module, which shows composite quotients refine both component quotients. In the Recognition Science framework this preserves the structure required by the Recognition Composition Law (the d'Alembert equation forcing multiplicative consistency) without invoking its explicit form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.