zorn_refinement_status
plain-language theorem explainer
The declaration defines a status string asserting that recognizer-induced equivalence relations on configuration space form a complete meet-semilattice under refinement, with composition supplying the infimum and Zorn's lemma securing maximal elements. Researchers constructing lattice structures for indistinguishability relations would cite this summary to confirm module completion. The definition assembles the string directly from enumerated properties without computation or lemma application.
Claim. The collection of equivalence relations induced by recognizers on configuration space forms a complete meet-semilattice under the refinement preorder, where the composition of recognizers yields the infimum of the induced relations and Zorn's lemma guarantees maximal elements in any chain-closed family.
background
In this module the RG3 indistinguishability axiom associates to each recognizer an equivalence relation on the configuration space. The induced relation is denoted recognizerSetoid and the refinement preorder is denoted IsFinerThan. Composition of recognizers supplies the meet operation, shown by the fact that the composite relation is the greatest lower bound of the two component relations. The local theoretical setting is the application of Zorn's lemma to chain-closed families of these relations, establishing a complete meet-semilattice with a minimum element, as described in the module documentation.
proof idea
The definition constructs a single concatenated string that lists the verified components: the map from recognizer to setoid, the left and right refinement inequalities under composition, the infimum characterization, the reflexivity and transitivity of the refinement preorder, and the existence of maximal elements via Zorn's lemma. It ends with an explicit completeness declaration. No tactics or external lemmas are invoked inside the definition; it functions as a static documentation constant.
why it matters
This definition encapsulates the module's results that formalize Theorem 4.1 and Theorem 5.1 of the paper on maximal recognizers and Zorn's lemma in Recognition Geometry. It confirms that the refinement preorder on recognizer-induced relations admits a complete meet-semilattice structure, supplying the lattice-theoretic foundation required for maximal partitions consistent with the indistinguishability axiom. The status string therefore closes the development of the refinement lattice within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.