composite_distinguishes
plain-language theorem explainer
The composite recognizer distinguishes any configuration pair that at least one component distinguishes. Researchers building multi-measurement models in Recognition Geometry cite this to establish that combined observations strictly refine the induced quotient. The term-mode proof unfolds distinguishability, rewrites the composite via its product equation, splits the resulting pair equality, and dispatches by case on the input disjunction.
Claim. Let $r_1 : Recognizer(C, E_1)$ and $r_2 : Recognizer(C, E_2)$. If $c_1, c_2$ in $C$ satisfy Distinguishable$(r_1, c_1, c_2) ∨$ Distinguishable$(r_2, c_1, c_2)$, then Distinguishable$(r_1 ⊗ r_2, c_1, c_2)$, where $r_1 ⊗ r_2$ denotes the product recognizer sending each configuration to the ordered pair of its images under $r_1$ and $r_2$.
background
In Recognition Geometry a recognizer is a map from configuration space $C$ to an emergence space $E$ that assigns to each configuration its recognized value. The composite of recognizers $r_1$ and $r_2$ is the product map $c ↦ (r_1(c), r_2(c))$. Distinguishability of $c_1$ and $c_2$ by $r$ means their images under $r$ differ. The module develops how such composites refine the quotient spaces induced by the individual recognizers. The module documentation states: 'When we combine two recognizers $R_1$ and $R_2$, we get a composite recognizer $R_{12}$ that can distinguish configurations that either $R_1$ or $R_2$ can distinguish.'
proof idea
The proof is a direct term-mode argument. It unfolds the definition of Distinguishable, introduces the assumption that the composite images are equal, rewrites using the sibling equation composite_R_eq that equates the composite to the product of the components, splits the pair equality via Prod.mk.injEq, and performs case analysis on the input disjunction to apply the corresponding component distinguishability predicate.
why it matters
This is the core lemma of the Refinement Theorem in Recognition Geometry (RG6). It is invoked directly by the downstream monotone-information results composite_info_monotone_left and composite_info_monotone_right, which establish that the composite carries at least as much distinguishing power as each component. The module positions the result as the mechanism by which richer geometry emerges from simpler measurements, consistent with the forcing chain that derives D = 3 and the eight-tick octave from the single functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.