pillar2_distinguish_monotone
plain-language theorem explainer
Distinguishability of configurations by a recognizer is preserved when that recognizer is composed with any second recognizer. Researchers working on recognition geometry cite this result to justify that adding recognizers refines distinctions without losing prior ones. The proof is a one-line wrapper that applies the left-monotonicity lemma for composite information.
Claim. If two configurations $c_1, c_2$ are distinguishable by recognizer $r_1$ (i.e., $r_1.R(c_1) ≠ r_1.R(c_2)$), then they remain distinguishable by the composite recognizer $r_1 ⊗ r_2$ for any recognizer $r_2$.
background
Configuration spaces are nonempty types of possible world states. Event spaces are types of observable outcomes required to be nontrivial (at least two distinct events). A recognizer is a map from configurations to events; two configurations are distinguishable by a recognizer precisely when they map to different events. Composite recognizers are formed by pairing two recognizers over the same configuration space, written $r_1 ⊗ r_2$ and defined in the Composition module. This theorem sits inside the module stating the three pillars of recognition geometry, where pillar 2 asserts that more recognizers yield finer resolution.
proof idea
The proof is a one-line wrapper that applies the composite_info_monotone_left lemma. That lemma in turn reduces to composite_distinguishes by injecting the left-hand distinguishability hypothesis via Or.inl.
why it matters
The result supplies the monotonicity half of pillar 2 in the foundational theorems of recognition geometry. It is invoked by the foundations_status summary that records the three pillars and the universal property of the recognition quotient. In the larger framework it confirms that the observable geometry extracted from a family of recognizers is stable under extension of that family, consistent with the principle that the quotient is the coequalizer of the indistinguishability relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.