ChainInfClosed
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.