maximal_cells_unsplittable
If recognizer r is maximal under refinement, meaning any finer r' must satisfy the reverse refinement, then r and r' induce identical indistinguishability on configurations. Lattice theorists applying Zorn's lemma to recognition geometries cite the result to equate cells of maximal elements. The proof is a one-line term application of the maximality hypothesis to the given pair.
claimLet $r:C→E$ and $r':C→E'$ be recognizers. Assume that whenever $r'$ refines $r$ (i.e., $r'≼r$), then $r$ refines $r'$ (i.e., $r≼r'$). If $c_1∼_r c_2$, then $r'≼r$ implies $c_1∼_{r'} c_2$, where $≼$ is the refinement order defined by inclusion of induced equivalence relations.
background
Recognition Geometry equips each recognizer with an equivalence relation on configuration space C via the RG3 indistinguishability axiom. The heterogeneous preorder IsFinerThan declares r1 finer than r2 precisely when every pair identified by r1 is identified by r2, i.e., the equivalence of r1 is contained in that of r2. The module uses this preorder to apply Zorn's lemma, guaranteeing maximal recognizers whose cells cannot be split further.
proof idea
The proof is a term-mode one-liner. It introduces the assumption that r' is finer than r, then applies that assumption directly to the pair c1, c2 under the supplied indistinguishability hypothesis for r.
why it matters in Recognition Science
The lemma is invoked by the downstream definition zorn_refinement_status to confirm that the family of recognizer setoids forms a complete meet-semilattice possessing a minimum element. It fills the uniqueness step in the paper's Theorem 4.1 on maximal recognizers, ensuring the refinement lattice is closed under the Zorn construction and that maximal cells are unambiguously defined.
scope and limits
- Does not prove existence of any maximal recognizer.
- Does not treat infinite descending refinement chains.
- Does not incorporate the Recognition Composition Law.
- Does not assign physical units or dimensions to C.
formal statement (Lean)
193theorem maximal_cells_unsplittable {E E' : Type*}
194 (r : Recognizer C E) (r' : Recognizer C E')
195 (hmax : IsFinerThan r' r → IsFinerThan r r')
196 (c₁ c₂ : C) (h : Indistinguishable r c₁ c₂) :
197 -- If r' is finer than r, then r is also finer than r'
198 -- meaning r and r' have exactly the same resolution cells
199 IsFinerThan r' r → Indistinguishable r' c₁ c₂ := by
proof body
Term-mode proof.
200 intro hfiner
201 exact hfiner c₁ c₂ h
202
203/-- If a maximal recognizer exists and another recognizer refines it,
204 they induce the same equivalence relation. -/