composite_indistinguishable_iff
plain-language theorem explainer
Two configurations are indistinguishable under a composite recognizer precisely when they are indistinguishable under each component. Recognition-geometry researchers cite the equivalence when establishing refinement and information monotonicity. The argument is a direct simplification that substitutes the product form of the composite map into the shared-event definition.
Claim. Let $r_1$ be a recognizer from configuration space $C$ to event space $E_1$ and $r_2$ a recognizer from $C$ to $E_2$. Configurations $c_1,c_2$ satisfy $c_1$ indistinguishable from $c_2$ under the composite $r_1⊗r_2$ if and only if they are indistinguishable under $r_1$ and under $r_2$.
background
Recognition Geometry module RG6 studies how multiple recognizers act on the same configuration space. The composite recognizer is defined by the product map $(r_1⊗r_2).R(c)=(r_1.R(c),r_2.R(c))$, as stated in the upstream theorem composite_R_eq. Indistinguishability is the equivalence relation that holds exactly when two configurations produce the same event under a given recognizer, per the definition in Indistinguishable. The module develops the refinement theorem showing that the composite distinguishes at least as much as either factor, yielding a finer quotient.
proof idea
The proof is a one-line term that applies simp to the definition of Indistinguishable, the equality composite_R_eq, and the injectivity of Prod.mk. This reduces the composite case directly to the conjunction of the two component equalities.
why it matters
The equivalence is invoked by composite_refines_left, composite_refines_right, composite_resolutionCell, and the extended fundamental theorem composite in RecogGeom.Foundations. It encodes the central claim of the module that richer geometry emerges from simultaneous measurements, and it supplies the logical step needed for the information-monotonicity results listed in composition_status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.