composite_setoid_iff
plain-language theorem explainer
The equivalence states that two configurations are indistinguishable under the composite recognizer if and only if they are indistinguishable under each component recognizer. Researchers establishing the meet-semilattice structure on recognizer setoids cite this when verifying that composition realizes the infimum operation. The argument is a direct one-line application of the indistinguishability characterization for composite recognizers.
Claim. Let $r_1 : C → E_1$ and $r_2 : C → E_2$ be recognizers and let $c_1, c_2 ∈ C$. Then $c_1$ is related to $c_2$ under the setoid induced by the composite recognizer $r_1 ⊗ r_2$ if and only if $c_1$ is related to $c_2$ under the setoid induced by $r_1$ and under the setoid induced by $r_2$.
background
In Recognition Geometry each recognizer induces an equivalence relation on configuration space C via the RG3 indistinguishability axiom; recognizerSetoid r is the resulting setoid (synonymous with indistinguishableSetoid). The composite recognizer $r_1 ⊗ r_2$ combines two recognizers, and the module shows that its induced setoid is the meet (infimum) in the refinement partial order on setoids. The local setting is the refinement lattice whose maximal elements are obtained via Zorn's Lemma, as stated in the module's reference to Theorems 4.1 and 5.1 of the paper on maximal recognizers.
proof idea
The proof is a one-line wrapper that applies composite_indistinguishable_iff from the Composition module, which supplies the corresponding equivalence for the indistinguishability relation of the composite recognizer.
why it matters
This equivalence is the key step used to prove composite_setoid_le_left, composite_setoid_le_right, composite_setoid_is_inf, and recognizer_meet_semilattice. The latter theorem states that composition provides the meet operation, so that a chain-closed family of recognizer setoids forms a complete meet-semilattice with a minimum element. It thereby supports the application of Zorn's Lemma to guarantee a finest recognizer setoid, directly filling the lattice-theoretic content of the paper's Theorem 4.1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.