maximal_recognizer_setoid_exists
plain-language theorem explainer
Any nonempty family P of setoids on configuration space C that is closed under infima of chains admits a minimal element m under the refinement order. Recognition geometers cite the result to guarantee a finest equivalence relation induced by recognizers within such families. The proof applies the Mathlib lemma zorn_nonempty_partialOrder₀ directly to the supplied chain-lower-bound hypothesis, extracting the minimal element in one term-mode step.
Claim. Let $P$ be a nonempty collection of setoids on configuration space $C$ such that every nonempty chain in $P$ possesses a lower bound in $P$ under the refinement preorder. Then there exists $m$ in $P$ with the property that for every $s$ in $P$, if $s$ refines $m$ then $m$ refines $s$.
background
In Recognition Geometry each recognizer induces an equivalence relation on configuration space $C$ via the RG3 indistinguishability axiom; the recognizerSetoid construction (synonym for indistinguishableSetoid) yields this setoid. The refinement preorder IsFinerThan orders these setoids so that composition corresponds to the infimum operation, as established by composite_setoid_is_inf together with the left and right refinement lemmas. The module therefore treats families of recognizer setoids as a preorder whose meets are realized by recognizer composition.
proof idea
The proof is a one-line wrapper that invokes zorn_nonempty_partialOrder₀ on P. The supplied lambda converts the hypothesis hchain into a lower-bound witness for any chain by packaging the obtained lb as an element of the subtype and verifying the bound property via Subtype.coe_injective. The final extraction step yields the minimal element satisfying the antisymmetry condition.
why it matters
The declaration is invoked by zorn_refinement_status, which concludes that any chain-closed family of recognizer setoids forms a complete meet-semilattice possessing a minimum element. It formalizes Theorems 4.1 and 5.1 of the paper on Maximal Recognizers and Zorn's Lemma in Recognition Geometry. Within the Recognition Science framework the result closes the refinement lattice for RG3-induced equivalences, ensuring that finest indistinguishability relations exist in any family closed under chain infima.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.