zorn_refinement_status
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove the refinement or infimum properties; those reside in separate theorems.
- Does not invoke or discharge Zorn's lemma; that step occurs in the maximal-element theorem.
- Does not connect the lattice structure to the forcing chain or physical constants.
- Does not supply a formal theorem; it only reports completion status via a string.
formal statement (Lean)
242def zorn_refinement_status : String :=
proof body
Definition body.
243 "✓ recognizerSetoid: Recognizer → Setoid C\n" ++
244 "✓ composite_setoid_le_left/right: composition refines both\n" ++
245 "✓ composite_setoid_is_inf: composition is greatest lower bound\n" ++
246 "✓ IsFinerThan: heterogeneous refinement preorder\n" ++
247 "✓ isFinerThan_refl, isFinerThan_trans: preorder properties\n" ++
248 "✓ composite_isFinerThan_left/right/glb: composition as meet\n" ++
249 "✓ maximal_recognizer_setoid_exists: ZORN'S LEMMA for recognizers\n" ++
250 "✓ maximal_cells_unsplittable: maximal cells are stable\n" ++
251 "✓ maximal_unique_setoid: maximal recognizers fix the partition\n" ++
252 "✓ recognizer_meet_semilattice: connection to complete lattice\n" ++
253 "\n" ++
254 "ZORN'S LEMMA + RG3 REFINEMENT: COMPLETE"
255
256#eval zorn_refinement_status
257
258end ZornRefinement
259end RecogGeom
260end IndisputableMonolith