composite_isFinerThan_left
plain-language theorem explainer
The theorem asserts that the composite recognizer refines its left component under the heterogeneous refinement preorder. Lattice theorists working on the meet-semilattice of recognizer setoids cite it when verifying that composition yields the infimum of two recognizers. The proof is a direct one-line term that unfolds the composite indistinguishability equivalence and projects its left conjunct.
Claim. Let $r_1 : C → E_1$ and $r_2 : C → E_2$ be recognizers. Then the composite $r_1 ⊗ r_2$ is finer than $r_1$: for all configurations $c_1, c_2 ∈ C$, if $c_1$ and $c_2$ are indistinguishable under the composite then they are indistinguishable under $r_1$.
background
In Recognition Geometry each recognizer induces an equivalence relation on configuration space $C$ via the indistinguishability predicate from the RG3 axiom. The IsFinerThan relation orders recognizers by inclusion of these equivalence relations: $r_1$ is finer than $r_2$ precisely when the equivalence classes of $r_1$ refine those of $r_2$. The module equips the collection of all such setoids with a partial order under which composition of recognizers acts as the meet (infimum) operation, as required for the application of Zorn's Lemma to maximal recognizers.
proof idea
The proof is a one-line term wrapper that invokes the upstream theorem composite_indistinguishable_iff on the input hypothesis and extracts the first conjunct, which is exactly the required indistinguishability under the left recognizer.
why it matters
This lemma supplies the left half of the claim that composition realizes the infimum in the refinement lattice, feeding directly into the downstream definition zorn_refinement_status that confirms the recognizer setoids form a complete meet-semilattice. It thereby supports the formalization of Theorems 4.1 and 5.1 in the paper on maximal recognizers and Zorn's Lemma, closing one step in the chain from the RG3 indistinguishability axiom to the existence of finest recognizers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.