isFinerThan_trans
plain-language theorem explainer
Refinement on recognizers is transitive: if R1 is finer than R2 and R2 is finer than R3 then R1 is finer than R3. Lattice theorists applying Zorn's lemma to the collection of recognizer-induced equivalences cite this to confirm the preorder. The proof is a one-line term that chains the two refinement hypotheses by composing their predicate implications.
Claim. If recognizer $R_1$ is finer than $R_2$ and $R_2$ is finer than $R_3$, then $R_1$ is finer than $R_3$, where finer means that the indistinguishability relation induced by the first recognizer is contained in the relation induced by the second.
background
In Recognition Geometry each recognizer $R: C → E$ induces an equivalence relation on configuration space $C$ via the RG3 indistinguishability axiom. The definition IsFinerThan states that $R_1$ is at least as fine as $R_2$ precisely when the equivalence of $R_1$ is a subset of the equivalence of $R_2$. The module treats the collection of all such equivalences as a partially ordered set under this refinement, with recognizer composition supplying the meet operation, to prepare the ground for Zorn's lemma.
proof idea
The proof is a one-line term-mode wrapper. It takes configurations $c_1, c_2$ and an indistinguishability witness $h$ under $r_1$, feeds $h$ into the first refinement hypothesis to obtain indistinguishability under $r_2$, then feeds that result into the second refinement hypothesis to obtain indistinguishability under $r_3$. No tactics or auxiliary lemmas are invoked.
why it matters
Transitivity completes the preorder axioms for IsFinerThan, which is required before Zorn's lemma can be applied to the family of recognizer setoids. The result feeds directly into zorn_refinement_status, which records that the structure is a complete meet-semilattice with a minimum element. This step realizes the lattice-theoretic content of Theorems 4.1 and 5.1 in the paper on maximal recognizers, supplying the preorder needed to guarantee finest recognizers in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.