recognizer_meet_semilattice
plain-language theorem explainer
Composition of two recognizers induces the infimum of their induced equivalence relations on configuration space. Researchers working on the refinement lattice in Recognition Geometry cite this to close the meet-semilattice structure before Zorn's lemma. The argument reduces the setoid equality by extensionality, simplifies infimum membership, and splits both directions via case analysis on the pair together with the composite characterization and one-sided refinement lemmas.
Claim. For recognizers $r_1 : C → E_1$ and $r_2 : C → E_2$, the equivalence relation induced by the composite recognizer $r_1 ⊗ r_2$ equals the infimum of the equivalence relations induced by $r_1$ and by $r_2$.
background
The module develops the refinement lattice of setoids induced by recognizers under the RG3 indistinguishability axiom. A recognizer $r : C → E$ induces the setoid recognizerSetoid r on configurations C, where two configurations are equivalent precisely when they map to the same event. Composition of recognizers $r_1 ⊗ r_2$ produces a new recognizer whose induced setoid refines both components. The local setting is the partially ordered collection of such setoids ordered by refinement (finer relations are smaller), with composition supplying the meet operation.
proof idea
The proof applies setoid extensionality to reduce the equality to relating pairs c1, c2. It simplifies the infimum definition via simp, then proves both directions. The forward direction cases on membership in the insert or singleton and applies the left or right refinement lemma. The converse extracts the relations under each component from the hypothesis and combines them using the composite iff characterization.
why it matters
This supplies the explicit meet operation for the lattice of recognizer setoids, which the module doc-comment identifies as the key step establishing a complete meet-semilattice with a minimum element when combined with the Zorn result. It feeds directly into the module status summary zorn_refinement_status. In the broader framework it realizes the infimum in the refinement preorder of equivalence relations arising from RG3, supporting the existence of maximal recognizers as in the referenced paper theorems 4.1 and 5.1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.