composite_isFinerThan_glb
plain-language theorem explainer
If recognizer r3 is finer than both r1 and r2 under the refinement order, then it is finer than their composite. Recognition geometers cite this to confirm that composition yields the greatest lower bound in the lattice of recognizer-induced setoids before applying Zorn's Lemma. The argument is a direct term-mode reduction that invokes the composite indistinguishability equivalence on the pair of facts supplied by the two hypotheses.
Claim. Let $r_1$, $r_2$, $r_3$ be recognizers on configuration space $C$. If the equivalence relation induced by $r_3$ is contained in the equivalence relations induced by $r_1$ and by $r_2$, then it is contained in the equivalence relation induced by the composite $r_1 ⊗ r_2$.
background
In Recognition Geometry each recognizer induces an equivalence relation on configurations via the indistinguishability predicate of axiom RG3. The IsFinerThan relation orders recognizers by refinement: r1 is at least as fine as r2 precisely when every pair indistinguishable under r1 remains indistinguishable under r2, i.e., the induced setoid of r1 refines that of r2. Composition of recognizers corresponds to the infimum operation in this poset, as the composite setoid is the meet of the component setoids.
proof idea
The proof is a one-line term that applies the mpr direction of the composite_indistinguishable_iff equivalence. The two IsFinerThan hypotheses supply the pair of indistinguishability facts for r1 and r2; the equivalence then yields indistinguishability under the composite.
why it matters
This result establishes that the composite realizes the glb in the IsFinerThan order, a prerequisite for the maximal_recognizer_setoid_exists theorem that invokes Zorn's Lemma. It fills the lattice property required by Theorem 5.1 in the paper on maximal recognizers and Zorn's Lemma in Recognition Geometry. The construction supports the forcing chain to T8 by guaranteeing that refinement steps remain discrete and closed under infima of chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.