maximal_recognizer_setoid_exists
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not construct the minimal element explicitly for any concrete family of recognizers.
- Does not apply to families lacking the chain-infimum closure hypothesis.
- Does not establish uniqueness of the minimal element.
- Does not address existence of maximal elements in the opposite order.
formal statement (Lean)
165theorem maximal_recognizer_setoid_exists
166 (P : Set (Setoid C))
167 (hne : P.Nonempty)
168 (hchain : ∀ (chain : Set (Setoid C)), chain ⊆ P → chain.Nonempty →
169 IsChain (· ≤ ·) chain → ∃ lb ∈ P, ∀ s ∈ chain, lb ≤ s) :
170 ∃ m ∈ P, ∀ s ∈ P, s ≤ m → m ≤ s := by
proof body
Term-mode proof.
171 -- Apply Zorn's Lemma in the ≤ order (where ≤ = "finer")
172 -- We need: every chain has a lower bound → minimal element exists
173 -- This is the standard dual Zorn formulation
174 obtain ⟨m, hmP, hm⟩ := zorn_nonempty_partialOrder₀ P
175 (fun chain hchain_sub hne_chain hchain_chain => by
176 obtain ⟨lb, hlb_mem, hlb_bound⟩ := hchain chain.toSet hchain_sub
177 ⟨hne_chain.some, hne_chain.some.2⟩
178 (fun a ha b hb hab => hchain_chain ha.2 hb.2 (Subtype.coe_injective.ne hab))
179 exact ⟨⟨lb, hlb_mem⟩, fun ⟨s, hs⟩ hs_chain => hlb_bound s hs_chain⟩)
180 hne
181 exact ⟨m, hmP, fun s hs hle => hm ⟨s, hs⟩ hle⟩
182
183/-! ## Section 6: Properties of Maximal Recognizers -/
184
185/-- A recognizer is *maximal* in a family if no other member properly refines it. -/