composite_setoid_is_inf
plain-language theorem explainer
The composite recognizer induces the infimum setoid in the refinement preorder on equivalence relations over configuration space. Researchers formalizing maximal recognizers via Zorn's lemma in Recognition Geometry cite this to equip the collection of setoids with a meet operation. The proof is a term construction that assembles the left and right refinement lemmas with the iff characterization of the composite setoid.
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$ satisfies $∼_{r_1 ⊗ r_2} ≤ ∼_{r_1}$, $∼_{r_1 ⊗ r_2} ≤ ∼_{r_2}$, and is the greatest such relation: any setoid $s$ with $s ≤ ∼_{r_1}$ and $s ≤ ∼_{r_2}$ also satisfies $s ≤ ∼_{r_1 ⊗ r_2}$.
background
In Recognition Geometry each recognizer induces an equivalence relation on configuration space $C$ via the RG3 indistinguishability axiom; recognizerSetoid $r$ denotes this setoid. The composite $r_1 ⊗ r_2$ is the recognizer whose event space is the product of the individual event spaces, and the refinement order on setoids is the heterogeneous preorder in which $s_1 ≤ s_2$ means $s_1$ is at least as fine as $s_2$ (i.e., $∼{s_1} ⊆ ∼{s_2}$). The module establishes that the collection of all such setoids forms a preorder whose binary meets are supplied by composition.
proof idea
The proof is a term-mode wrapper. It applies composite_setoid_le_left and composite_setoid_le_right to obtain the two lower-bound conjuncts, then discharges the universal quantifier by invoking composite_setoid_iff to convert the assumption that $s$ refines both components into the claim that $s$ refines the composite.
why it matters
This result supplies the meet operation for the refinement preorder, which zorn_refinement_status invokes to conclude that the family of recognizer setoids is a complete meet-semilattice with a minimum element. It thereby completes the lattice-theoretic prerequisite for applying Zorn's lemma to obtain maximal recognizers, as required by Theorems 4.1 and 5.1 of the paper on Maximal Recognizers and Zorn's Lemma in Recognition Geometry. The construction directly supports the RG3 axiom by ensuring the partial order on indistinguishability relations admits extremal arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.