composite_info_monotone_left
plain-language theorem explainer
If one recognizer distinguishes two configurations, the composite with any second recognizer distinguishes them as well. Researchers proving the refinement theorem in recognition geometry cite this monotonicity. The proof is a one-line wrapper that feeds the left distinguishability hypothesis into the general composite_distinguishes lemma.
Claim. Let $r_1$ be a recognizer from configurations $C$ to events $E_1$ and $r_2$ a recognizer from $C$ to $E_2$. For $c_1,c_2$ in $C$, if $r_1.R(c_1)neq r_1.R(c_2)$ then $(r_1otimes r_2).R(c_1)neq(r_1otimes r_2).R(c_2)$.
background
In the Recognition Geometry module on composition, a Recognizer is a map sending configurations in $C$ to events in some space $E$. Distinguishability of $c_1$ and $c_2$ under recognizer $r$ means $r.R(c_1)neq r.R(c_2)$. The composite $r_1otimes r_2$ is the recognizer that returns the ordered pair of events from both components, so its recognition map satisfies the equality recorded in composite_R_eq.
proof idea
One-line wrapper that applies composite_distinguishes to the disjunction formed by injecting the given left distinguishability hypothesis via Or.inl.
why it matters
The result is invoked directly by pillar2_distinguish_monotone in Foundations, which records the corollary that distinguishability is monotonic under composition. It supplies the left half of the Refinement Theorem whose module documentation states that the composite quotient refines both component quotients. In the Recognition Science framework this supports emergence of richer geometry from multiple measurements, consistent with the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.