composite_setoid_le_left
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish the symmetric refinement property with respect to the second recognizer.
- Does not prove that the composite setoid is the greatest lower bound.
- Does not construct or exhibit a maximal recognizer.
- Does not invoke Zorn's Lemma or any chain-completeness argument.
formal statement (Lean)
62theorem composite_setoid_le_left {E₁ E₂ : Type*}
63 (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
64 recognizerSetoid (r₁ ⊗ r₂) ≤ recognizerSetoid r₁ :=
proof body
Term-mode proof.
65 fun h => ((composite_setoid_iff r₁ r₂ _ _).mp h).1
66
67/-- **Refinement Right**: The composite setoid is at least as fine as r₂'s. -/