composite_info_monotone_right
plain-language theorem explainer
If recognizer r₂ distinguishes configurations c₁ and c₂ then the composite recognizer r₁ ⊗ r₂ also distinguishes them. Researchers modeling measurement refinement in Recognition Geometry cite this when showing that a second channel strictly increases distinguishing power. The proof is a one-line term application of the general composite_distinguishes lemma to the right disjunct of the hypothesis.
Claim. Let $r_1$ and $r_2$ be recognizers on configuration space $C$. If $r_2$ distinguishes $c_1$ and $c_2$, then the composite recognizer $r_1 ⊗ r_2$ distinguishes $c_1$ and $c_2$.
background
The module develops the theory of composite recognizers under the Recognition Composition Law. A Recognizer maps configurations in $C$ to events in some type $E$; two configurations are Distinguishable when they produce unequal events. The composite $r_1 ⊗ r_2$ is defined by the product map sending $c$ to the pair of events $(r_1(c), r_2(c))$, so the composite distinguishes precisely when at least one component does. The upstream composite_distinguishes theorem states that the composite distinguishes any pair that either component distinguishes.
proof idea
The proof is a one-line wrapper that applies composite_distinguishes to the disjunction formed by injecting the given hypothesis into the right summand.
why it matters
The declaration supplies the right-monotonicity half of the refinement property for composite recognizers, directly supporting the module's Refinement Theorem that the composite quotient is finer than either component quotient. It illustrates how richer geometry emerges from combining independent measurements, consistent with the eight-tick octave and phi-ladder structure in the broader Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.