IsFinerThan
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not require the event types of the two recognizers to coincide.
- Does not assert that the relation is antisymmetric or a total order.
- Does not incorporate any metric or topological structure on configuration space C.
- Does not presuppose any particular properties of the recognizer map beyond the induced indistinguishability relation.
formal statement (Lean)
101def IsFinerThan {E₁ E₂ : Type*} (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) : Prop :=
proof body
Definition body.
102 ∀ c₁ c₂ : C, Indistinguishable r₁ c₁ c₂ → Indistinguishable r₂ c₁ c₂
103
104/-- Refinement is reflexive. -/