IsMaximalRecognizer
A recognizer r is maximal in a family if no other recognizer r' in the family properly refines it under the refinement preorder. Researchers working on the lattice of equivalence relations induced by the RG3 indistinguishability axiom would cite this definition when invoking Zorn's Lemma to obtain a finest recognizer. The definition is a direct universal quantification that encodes maximality via the IsFinerThan relation without additional lemmas.
claimLet $r$ be a recognizer from configuration space $C$ to type $E$. Let $F$ assign to each type $E'$ a set of recognizers to $E'$. Then $r$ is maximal in $F$ if, for all $E'$ and all $r'$ in $F(E')$, whenever $r'$ refines $r$ then $r$ refines $r'$.
background
The module connects Zorn's Lemma to the RG3 axiom of Recognition Geometry. Each recognizer induces an equivalence relation on configuration space $C$ via indistinguishability, and the collection of such relations is partially ordered by refinement, with composition corresponding to the meet operation. The refinement preorder IsFinerThan is defined in the same module, with reflexivity and transitivity proved separately as isFinerThan_refl and isFinerThan_trans. Composite recognizers produce finer setoids, as shown by composite_setoid_le_left and composite_setoid_is_inf.
proof idea
This is the primitive definition of the maximality predicate. It directly states the universal condition over all $E'$ and $r'$ in the family: if IsFinerThan r' r then IsFinerThan r r'. No upstream lemmas are invoked; the body is the explicit forall statement that captures the non-proper-refinement property.
why it matters in Recognition Science
This definition is the prerequisite for maximal_recognizer_setoid_exists, which applies Zorn's Lemma to guarantee a finest recognizer in the refinement lattice. It formalizes the core of Theorem 4.1 and Theorem 5.1 from the paper on Maximal Recognizers and Zorn's Lemma in Recognition Geometry. In the Recognition Science framework it supports the construction of maximal elements under the RG3-induced partial order, preparing the ground for the existence of an indisputable finest resolution.
scope and limits
- Does not assert existence of a maximal recognizer.
- Does not require the family to be nonempty or chain-complete.
- Does not specify how recognizers arise from physical spectra or phi-ladder data.
- Does not prove that refinement is a partial order (handled by sibling lemmas).
formal statement (Lean)
186def IsMaximalRecognizer {E : Type*} (r : Recognizer C E)
187 (family : ∀ (E' : Type*), Set (Recognizer C E')) : Prop :=
proof body
Definition body.
188 ∀ (E' : Type*) (r' : Recognizer C E'), r' ∈ family E' →
189 IsFinerThan r' r → IsFinerThan r r'
190
191/-- A maximal recognizer has the property that its resolution cells cannot
192 be split by any other recognizer in the family. -/