composite_refines_right
If two configurations are indistinguishable under the composite recognizer r1 ⊗ r2, then they remain indistinguishable under r2 alone. Researchers constructing natural maps between recognition quotients cite this when showing that the composite quotient projects onto each factor. The proof is a direct one-line extraction of the second conjunct from the biconditional supplied by composite_indistinguishable_iff.
claimIf $c_1$ and $c_2$ satisfy $c_1 ~[r_1 ⊗ r_2] c_2$, then $c_1 ~[r_2] c_2$.
background
Recognition geometry equips a configuration space C with a recognizer r : Recognizer C E that sends each configuration to an event in E. Indistinguishability is the kernel relation: c1 ~[r] c2 precisely when r.R c1 = r.R c2. The module develops composite recognizers r1 ⊗ r2 whose event space is the product E1 × E2 and whose action is the paired map c ↦ (r1(c), r2(c)). The central result is that the composite induces a strictly finer equivalence than either factor, so its quotient is larger. This theorem supplies the right-projection half of that refinement. It rests on the explicit biconditional composite_indistinguishable_iff, which states that indistinguishability under the composite holds exactly when both components agree.
proof idea
The proof is a one-line term wrapper. It applies the forward direction of composite_indistinguishable_iff to the hypothesis h, obtaining the conjunction of the two component indistinguishabilities, then selects the second conjunct.
why it matters in Recognition Science
The declaration is invoked inside the definition of quotientMapRight to witness that the lifted map from the composite quotient to the r2 quotient is well-defined. Together with its left counterpart it completes the refinement theorem of the module, showing that the composite quotient refines both component quotients. In the broader Recognition Science setting this supplies the geometric mechanism by which multiple measurements generate richer structure, consistent with the composition law and the emergence of D = 3 from the eight-tick octave.
scope and limits
- Does not prove the symmetric refinement statement for the left recognizer r1.
- Does not establish surjectivity of the induced quotient maps.
- Does not extend to recognizers whose event spaces are not products.
- Does not quantify over the concrete form of the event types E1 and E2.
Lean usage
quotientMapRight r1 r2 (Quotient.mk (r1 ⊗ r2) c)formal statement (Lean)
74theorem composite_refines_right (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
75 {c₁ c₂ : C} (h : Indistinguishable (r₁ ⊗ r₂) c₁ c₂) :
76 Indistinguishable r₂ c₁ c₂ :=
proof body
Term-mode proof.
77 ((composite_indistinguishable_iff r₁ r₂ c₁ c₂).mp h).2
78
79/-- The composite distinguishes configs that either component distinguishes -/