composite_refines_left
plain-language theorem explainer
If two configurations are indistinguishable under the composite recognizer r1 ⊗ r2, then they remain indistinguishable under r1. Recognition-geometry researchers cite this when showing that joint measurements refine single recognizers and enlarge the quotient. The proof is a one-line term that applies the composite-indistinguishability equivalence and projects to its left conjunct.
Claim. Let $r_1 : C → E_1$ and $r_2 : C → E_2$ be recognizers. If $c_1, c_2 ∈ C$ satisfy $r_1(c_1) = r_1(c_2)$ and $r_2(c_1) = r_2(c_2)$, then $r_1(c_1) = r_1(c_2)$.
background
Recognition geometry studies the equivalence relation Indistinguishable r c1 c2, defined by r.R c1 = r.R c2. The composite recognizer r1 ⊗ r2 is the product map sending c to (r1(c), r2(c)). The module develops the refinement theorem for such composites: the joint recognizer distinguishes at least as much as either factor. The upstream lemma composite_indistinguishable_iff states that indistinguishability under the composite holds if and only if it holds under both components.
proof idea
The term applies composite_indistinguishable_iff to the hypothesis h and extracts the first conjunct of the resulting conjunction.
why it matters
This theorem supplies the left half of the refinement property used by quotientMapLeft to construct the natural projection from the composite quotient onto the r1 quotient. It appears in the module's composition_status summary and contributes to the Refinement Theorem of RG6, which shows how richer geometry emerges from simultaneous measurements. The result is part of the chain establishing that composite quotients refine their factors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.