maximal_unique_setoid
plain-language theorem explainer
If a recognizer r₂ refines r₁ and r₁ satisfies maximality (any refinement of r₂ forces the reverse), then the two recognizers induce identical equivalence relations on configuration space C. Researchers formalizing the refinement lattice of Recognition Geometry cite this to establish uniqueness of maximal elements under the RG3 axiom. The proof is a one-line term-mode argument that applies setoid extensionality and invokes the two refinement hypotheses in each direction.
Claim. Let $r_1 : C → E_1$ and $r_2 : C → E_2$ be recognizers. If $r_2$ is finer than $r_1$ (i.e., whenever $r_2$ identifies $c_1, c_2$ then so does $r_1$) and maximality holds (fineness of $r_2$ over $r_1$ implies the converse), then the induced setoids coincide: recognizerSetoid $r_1$ = recognizerSetoid $r_2$.
background
The module applies Zorn's Lemma to the partial order of recognizer-induced setoids on configuration space C. Each recognizer R : C → E induces an equivalence ~R via the RG3 indistinguishability axiom; recognizerSetoid is the synonym for this induced setoid. IsFinerThan r₁ r₂ holds when ~{r₁} ⊆ ~_{r₂}, i.e., r₁ is at least as fine as r₂. Composition of recognizers supplies the meet operation, making the collection a sub-meet-semilattice. Upstream results on the Recognition Composition Law and d'Alembert factorization supply the algebraic compatibility needed for the lattice operations.
proof idea
The term proof applies setoid extensionality, reducing equality to mutual inclusion of the indistinguishability predicates. The forward direction invokes the hypothesis that r₂ is finer than r₁; the converse applies the maximality hypothesis to the given fineness assumption. No additional lemmas are required beyond the definition of IsFinerThan.
why it matters
The theorem supplies the uniqueness half of the Zorn argument, feeding directly into zorn_refinement_status which concludes that recognizer setoids form a complete meet-semilattice possessing a minimum element. It realizes the lattice-theoretic content of Theorem 4.1 in the Recognition Geometry paper, confirming that the chain-closed family has a unique finest recognizer. The result closes the uniqueness gap required before the eight-tick octave and D = 3 spatial dimensions can be extracted from the bottom element.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.