ChainInfClosed
ChainInfClosed encodes the chain-infimum closure condition for a family of setoids on configuration space C. Researchers applying Zorn's Lemma to the refinement poset of recognizer equivalences cite this definition to establish existence of maximal elements. It directly states that the infimum of any nonempty chain within the family remains inside the family, enabling the dual-Zorn argument for minimal recognizers.
claimA family $P$ of setoids on configuration space $C$ is chain-infimum closed when, for every nonempty chain $C'subseteq P$ under the refinement partial order, the greatest lower bound $inf C'$ lies in $P$.
background
Recognition Geometry associates each recognizer with an equivalence relation on configuration space C via the indistinguishability axiom RG3. The module equips the collection of such setoids with the refinement order, under which composition of recognizers corresponds to the meet operation. ChainInfClosed captures the lattice-theoretic property that this collection is closed under infima of chains, a prerequisite for invoking Zorn's Lemma.
proof idea
ChainInfClosed is introduced as a direct definition. It unfolds the universal quantifier over chains, requiring that the setoid infimum operation sInf maps any qualifying chain back into P. No lemmas are applied; the body is the explicit predicate.
why it matters in Recognition Science
This definition supplies the key hypothesis for the application of Zorn's Lemma in the refinement lattice, as referenced in the module's main result maximal_recognizer_setoid_exists. It formalizes the dual of Zorn's Lemma for minimal elements in the poset of recognizer setoids, directly supporting Theorem 4.1 and 5.1 of the paper on Maximal Recognizers. The construction ties into the RG3 axiom and the partial order induced by recognizer composition.
scope and limits
- Does not assert that any particular family P satisfies the closure property.
- Does not construct the infimum explicitly or prove its existence.
- Does not address maximality or minimality of elements in P.
- Does not depend on specific properties of the configuration space C beyond setoid structure.
formal statement (Lean)
153def ChainInfClosed (P : Set (Setoid C)) : Prop :=
proof body
Definition body.
154 ∀ (chain : Set (Setoid C)), chain ⊆ P → chain.Nonempty → IsChain (· ≤ ·) chain →
155 sInf chain ∈ P
156
157/-- **Theorem (Zorn for Recognizers)**: Let P be a nonempty family of setoids
158 on C that is closed under chain infima. Then P contains a minimal element—
159 a finest recognizer-induced equivalence relation.
160
161 Formally: ∃ m ∈ P such that no s ∈ P is strictly finer than m.
162
163 This is the dual of Zorn's Lemma (existence of minimal elements):
164 every chain has a lower bound (the infimum) ⟹ minimal element exists. -/