composite_setoid_le_right
Composite recognizer setoids refine the right component's setoid in the refinement preorder. Researchers formalizing the lattice of recognizers cite this lemma when constructing the meet operation ahead of Zorn applications. The term proof extracts the right conjunct from the composite setoid equivalence.
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$ refines the equivalence relation induced by $r_2$.
background
Recognition Geometry associates to each recognizer an equivalence relation on configuration space C via the RG3 indistinguishability axiom. The recognizerSetoid is this induced equivalence (synonym for indistinguishableSetoid), and composition ⊗ of recognizers corresponds to the meet in the refinement lattice of setoids. The module prepares these refinement properties for Zorn's lemma applications to maximal recognizers.
proof idea
One-line term proof that applies the composite_setoid_iff characterization and projects to the second component of the resulting conjunction.
why it matters in Recognition Science
This lemma is a direct prerequisite for composite_setoid_is_inf, which establishes the infimum property, and for recognizer_meet_semilattice, which shows recognizer setoids form a meet-semilattice. It supplies the refinement facts needed to apply Zorn's lemma for existence of maximal recognizers, as referenced in the module documentation for Theorems 4.1 and 5.1.
scope and limits
- Does not establish the left refinement for r1.
- Does not prove the full infimum property.
- Does not invoke Zorn's lemma.
- Does not depend on phi-ladder or physical constants.
formal statement (Lean)
68theorem composite_setoid_le_right {E₁ E₂ : Type*}
69 (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
70 recognizerSetoid (r₁ ⊗ r₂) ≤ recognizerSetoid r₂ :=
proof body
Term-mode proof.
71 fun h => ((composite_setoid_iff r₁ r₂ _ _).mp h).2
72
73/-! ## Section 3: The Infimum (Meet) Property
74
75The composite setoid is the greatest lower bound (infimum) of the two
76component setoids in the lattice of setoids on C. -/
77
78/-- **Infimum Property**: The composite setoid is the greatest setoid
79 that is at least as fine as both r₁ and r₂. -/