IsFinerThan
plain-language theorem explainer
IsFinerThan encodes the heterogeneous refinement preorder on recognizers: r1 is at least as fine as r2 precisely when every pair indistinguishable under r1 remains indistinguishable under r2. Researchers establishing maximal recognizers via Zorn's lemma cite this relation to equip the collection of all recognizers with a partial order. The definition is introduced directly as the subset relation on the induced equivalence classes.
Claim. Let $r_1 : C → E_1$ and $r_2 : C → E_2$ be recognizers. Then $r_1$ is finer than $r_2$ if and only if for all configurations $c_1, c_2 ∈ C$, $r_1(c_1) = r_1(c_2)$ implies $r_2(c_1) = r_2(c_2)$.
background
In Recognition Geometry a recognizer maps configurations in space $C$ to events in some type $E$, inducing the fundamental equivalence $c_1 ∼_r c_2$ exactly when the recognizer outputs coincide. The module builds the refinement lattice on these equivalences so that composition of recognizers yields the meet operation, directly supporting the RG3 indistinguishability axiom and the subsequent application of Zorn's lemma. The upstream Indistinguishable predicate is defined by equality of recognizer outputs and supplies the concrete relation appearing inside the universal quantifier.
proof idea
The declaration is a direct definition that packages the universal quantification over configuration pairs using the Indistinguishable predicate.
why it matters
This definition supplies the partial order required for the refinement lattice. It is invoked to establish reflexivity and transitivity of refinement, to prove that composites are finer than each factor, and to define the notion of a maximal recognizer. It thereby fills the role of the refinement relation in the module's Theorems 4.1 and 5.1 on maximal recognizers and Zorn's lemma, enabling selection of finest recognizers consistent with the eight-tick octave and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.