pillar2_information_monotonicity
plain-language theorem explainer
Pillar 2 establishes that two configurations are indistinguishable under the composite recognizer r1 ⊗ r2 exactly when they are indistinguishable under r1 and under r2 separately. Researchers formalizing observable geometry or the recognition quotient cite this monotonicity result as one of the three foundational pillars. The proof is a direct one-line application of the composite indistinguishability equivalence.
Claim. For a configuration space $C$ equipped with event spaces $E_1$ and $E_2$, and recognizers $r_1 : C → E_1$, $r_2 : C → E_2$, two configurations $c_1, c_2 ∈ C$ satisfy indistinguishability under the composite recognizer if and only if they satisfy it under each component recognizer separately.
background
Recognition Geometry rests on three pillars. Pillar 2 asserts that adding recognizers can only increase distinguishing power, so the recognition quotient $C_R$ becomes finer. A ConfigSpace supplies an empty configuration, a commutative join operation, a consistency predicate, and an independence relation. The local setting is the module stating the Fundamental Theorems, where the observable geometry of any configuration space is completely determined by its family of recognizers via the equivalence $[c_1] = [c_2]$ in $C_R$ iff $R(c_1) = R(c_2)$.
proof idea
One-line wrapper that applies composite_indistinguishable_iff from the Composition module.
why it matters
The result is invoked by foundations_status to certify the three pillars. It supplies the information-monotonicity step required for the universal property of the recognition quotient. The statement aligns with the Recognition Composition Law and supports the claim that the quotient is the coequalizer of the indistinguishability relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.