maximal_unique_setoid
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of any maximal recognizer.
- Does not apply when the maximality hypothesis is absent.
- Does not treat setoids outside the recognizer-induced family.
- Does not address algorithmic construction of the maximal element.
formal statement (Lean)
205theorem maximal_unique_setoid {E₁ E₂ : Type*}
206 (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
207 (hfiner : IsFinerThan r₂ r₁)
208 (hmax : IsFinerThan r₂ r₁ → IsFinerThan r₁ r₂) :
209 recognizerSetoid r₁ = recognizerSetoid r₂ := by
proof body
Term-mode proof.
210 ext c₁ c₂
211 exact ⟨fun h => hfiner c₁ c₂ h, fun h => hmax hfiner c₁ c₂ h⟩
212
213/-! ## Section 7: Connection to the Complete Lattice
214
215The setoids on C form a complete lattice in Mathlib. The recognizer-induced
216setoids form a sub-meet-semilattice (closed under finite meets via ⊗).
217The Zorn result above shows that with the chain-infimum closure property,
218this sublattice has a bottom element (finest recognizer). -/
219
220/-- Composition provides the meet (infimum) operation for recognizer setoids.
221 Together with the Zorn result, this establishes that a chain-closed
222 family of recognizer setoids forms a complete meet-semilattice with
223 a minimum element. -/