composite_setoid_is_inf
The composite recognizer induces the infimum setoid in the refinement preorder on equivalence relations over configuration space. Researchers formalizing maximal recognizers via Zorn's lemma in Recognition Geometry cite this to equip the collection of setoids with a meet operation. The proof is a term construction that assembles the left and right refinement lemmas with the iff characterization of the composite setoid.
claimLet $r_1 : C → E_1$ and $r_2 : C → E_2$ be recognizers. The equivalence relation induced by the composite recognizer $r_1 ⊗ r_2$ satisfies $∼_{r_1 ⊗ r_2} ≤ ∼_{r_1}$, $∼_{r_1 ⊗ r_2} ≤ ∼_{r_2}$, and is the greatest such relation: any setoid $s$ with $s ≤ ∼_{r_1}$ and $s ≤ ∼_{r_2}$ also satisfies $s ≤ ∼_{r_1 ⊗ r_2}$.
background
In Recognition Geometry each recognizer induces an equivalence relation on configuration space $C$ via the RG3 indistinguishability axiom; recognizerSetoid $r$ denotes this setoid. The composite $r_1 ⊗ r_2$ is the recognizer whose event space is the product of the individual event spaces, and the refinement order on setoids is the heterogeneous preorder in which $s_1 ≤ s_2$ means $s_1$ is at least as fine as $s_2$ (i.e., $∼{s_1} ⊆ ∼{s_2}$). The module establishes that the collection of all such setoids forms a preorder whose binary meets are supplied by composition.
proof idea
The proof is a term-mode wrapper. It applies composite_setoid_le_left and composite_setoid_le_right to obtain the two lower-bound conjuncts, then discharges the universal quantifier by invoking composite_setoid_iff to convert the assumption that $s$ refines both components into the claim that $s$ refines the composite.
why it matters in Recognition Science
This result supplies the meet operation for the refinement preorder, which zorn_refinement_status invokes to conclude that the family of recognizer setoids is a complete meet-semilattice with a minimum element. It thereby completes the lattice-theoretic prerequisite for applying Zorn's lemma to obtain maximal recognizers, as required by Theorems 4.1 and 5.1 of the paper on Maximal Recognizers and Zorn's Lemma in Recognition Geometry. The construction directly supports the RG3 axiom by ensuring the partial order on indistinguishability relations admits extremal arguments.
scope and limits
- Does not prove existence of maximal recognizers (requires Zorn's lemma separately).
- Does not treat infinite meets or arbitrary families of recognizers.
- Does not establish that the refinement relation is antisymmetric.
- Does not address computational realizability of the composite recognizer.
formal statement (Lean)
80theorem composite_setoid_is_inf {E₁ E₂ : Type*}
81 (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
82 -- (1) composite ≤ r₁
83 recognizerSetoid (r₁ ⊗ r₂) ≤ recognizerSetoid r₁ ∧
84 -- (2) composite ≤ r₂
85 recognizerSetoid (r₁ ⊗ r₂) ≤ recognizerSetoid r₂ ∧
86 -- (3) greatest: any s ≤ r₁ and s ≤ r₂ implies s ≤ composite
87 ∀ (s : Setoid C), s ≤ recognizerSetoid r₁ → s ≤ recognizerSetoid r₂ →
88 s ≤ recognizerSetoid (r₁ ⊗ r₂) := by
proof body
Term-mode proof.
89 refine ⟨composite_setoid_le_left r₁ r₂, composite_setoid_le_right r₁ r₂, ?_⟩
90 intro s h₁ h₂ hs
91 exact (composite_setoid_iff r₁ r₂ _ _).mpr ⟨h₁ hs, h₂ hs⟩
92
93/-! ## Section 4: Refinement as a Preorder
94
95We define an explicit "is at least as fine as" relation on recognizers
96that works across different event types. -/
97
98/-- R₁ is *at least as fine as* R₂: whenever R₁ identifies two configurations,
99 R₂ also identifies them. Equivalently, ~_{R₁} ⊆ ~_{R₂} as sets of pairs.
100 This is the heterogeneous refinement relation (event types may differ). -/