composite_isFinerThan_right
plain-language theorem explainer
Composite recognizers are finer than their right-hand factor under the refinement preorder of Recognition Geometry. Lattice theorists studying indistinguishability relations cite this when verifying that tensor product supplies a lower bound. The proof reduces directly to the second conjunct of the biconditional for indistinguishability under the composite.
Claim. For recognizers $r_1 : C → E_1$ and $r_2 : C → E_2$, indistinguishability under the composite $r_1 ⊗ r_2$ implies indistinguishability under $r_2$.
background
Recognition Geometry equips each recognizer with an indistinguishability equivalence on configuration space C via the RG3 axiom. The predicate IsFinerThan holds when the equivalence of the first recognizer refines that of the second: whenever the first identifies a pair the second does as well. Composition of recognizers is defined so that a pair is indistinguishable under the composite precisely when it is under each factor.
proof idea
A direct term proof applies the right conjunct after rewriting the hypothesis via the forward implication of composite_indistinguishable_iff.
why it matters
It supplies one direction of the infimum property for the composite in the refinement poset, as required for the lattice structure underlying the application of Zorn's Lemma. The module formalizes results from the paper on maximal recognizers. This step confirms that the tensor product yields a lower bound in the preorder of recognizers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.