composite_setoid_le_left
plain-language theorem explainer
The theorem shows that the equivalence relation induced by a composite recognizer refines the relation induced by its first component alone. Researchers constructing the refinement poset of recognizer setoids cite this when verifying that composition yields lower bounds. The proof is a direct one-line term extraction of the left conjunct from the biconditional supplied by the companion characterization lemma.
Claim. Let $r_1 : C → E_1$ and $r_2 : C → E_2$ be recognizers. The equivalence relation induced by the composite recognizer $r_1 ⊗ r_2$ refines the equivalence relation induced by $r_1$: if two configurations are related under the composite setoid then they are related under the setoid of $r_1$.
background
In Recognition Geometry each recognizer $r : C → E$ induces an equivalence relation on configuration space $C$ via the RG3 indistinguishability axiom; recognizerSetoid $r$ is the corresponding setoid (synonymous with indistinguishableSetoid). Composition $r_1 ⊗ r_2$ is the operation whose induced setoid is intended to act as the meet in the refinement order on these setoids. The module applies Zorn's Lemma to the poset of all such setoids ordered by refinement, establishing existence of maximal elements.
proof idea
The proof is a one-line term-mode wrapper. It applies the forward direction of composite_setoid_iff to the hypothesis that the pair is related under the composite setoid, then projects the first conjunct of the resulting conjunction, which is precisely membership in recognizerSetoid $r_1$.
why it matters
This supplies the left half of the lower-bound claim for composite setoids. It is invoked directly inside composite_setoid_is_inf to establish that the composite is a lower bound for both components, and thereby inside recognizer_meet_semilattice to equate composition with the set-theoretic infimum. These steps close the meet-semilattice structure required for the Zorn application recorded in zorn_refinement_status. The result formalizes part of Theorem 4.1 in the paper on Maximal Recognizers and Zorn's Lemma, linking the RG3 axiom to the refinement lattice whose maximal element corresponds to a finest recognizer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.